#ifndef FRAIG_H
#define FRAIG_H

#include "cktcover.h"
#include "msatsolver.h"

#define PATSIZE 128
#define RUNRUN 20

class Pattern;

struct Array{
   unsigned sz;
   unsigned * dat;
   Array():sz(0){}
};
/**
@brief Fraig 

fraig performs 
a) simulation , partition 
b) dump cnf to solver
c) selection to prove eq
d) feedback pattern to partition
*/
class Fraig : public CktCover
{
   Pattern  * _pats;
   
   unsigned * _eqn;      ///< equivalent group
   int * _group;    ///< dual buffer to _ngroup 
   int * _ngroup;   ///< dual buffer to _group
   int * _idx;      ///<
   int * _deplvl;   ///< dependency level of literal in group

   // State of feedback
   //
   int      _npat;  ///< number of pattern feedback 
   int      _selptr;///< select ptr 
   int      _end;   ///< end of select ptr

   vec<Array> _stages;///< dependency grouping of the candidate

   MinisatSolver _solver;

   // fill for simulation 
   void pat_init_rand();
   void sat2pat_input();
   void sat2pat_eqset();
   void simulation();
   void reset_selection();

   // partition
   int partition(bool fold );
   void rm_eq_partition();   ///< remove the proved eq class ( which is setted by rm_eq setted by )
   void grouping();          ///< random simulation to partition
   void eq_dep_level();      ///< compute the dependency level 

   // Selction 
   //
   int select_sig();
   void rm_eq();

   bool prove_eq( int , int );
   int  prove_eq_limit( int , int );
   void skip();
   
   void report();
   void cover_clause();

   void feedback();
   void feedback2();
   void merge();

   public:
   ~Fraig();

   void init();
   void run();
   void run2();
};

#endif
